단순 타입 λ-계산
- λ-계산
- 연역 체계
단순 타입 λ-계산(simply typed λ-calculus, STLC)는 함수 타입, 곱 타입, 합 타입, 자연수 타입 등을 허용하는 간단한 타입 체계를 갖춘 λ-계산이다. 커리-하워드 대응 관점에서 단순 타입 λ-계산은 자연 연역 방식 명제 논리 체계의 일종으로 볼 수 있다.
단순 타입 λ-계산(simply typed λ-calculus, STLC)는 함수 타입, 곱 타입, 합 타입, 자연수 타입 등을 허용하는 간단한 타입 체계를 갖춘 λ-계산이다. 커리-하워드 대응 관점에서 단순 타입 λ-계산은 자연 연역 방식 명제 논리 체계의 일종으로 볼 수 있다.